$\forall$$p$,$q$:$\mathbb{Z}$. gcd\_reduce($p$; $q$) $\in$ (:$\mathbb{N}$ $\times$ (:$\mathbb{Z}$ $\times$ $\mathbb{Z}$))